Iof proof for Lemma add mono wrt eq rw:
a, b, n:
. {(a = b) 
(a+n = b+n)}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_eq`))
C.| 12,41 |
a, b, n:. {(a = b) (a+n = b+n)}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_eq`))
C.
| Definitions | |
| Lemmas |